Lambda the Ultimate

As you can probably deduce from the lack of posts, I am extremely busy. Real life is taking its toll.

I implore the other editors to take charge.

EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version. Kwangkeun Yi. JFP. 16(6):663-670.

Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for developing programs with an article in this journal. Unfortunately, his example uses both higher-order functions and continuation-passing style, which is too difficult for students in an introductory programming course. In this pearl, we present a first-order version of Harper's example and demonstrate that it is easy to transform the final version into an efficient state machine. Our new version convinces students that the approach is useful, even essential, in developing both correct and efficient programs.

The problem is regular expression matching: checking whether a string S belongs to the language specified by the regular expression r.

Bjarne Stroustrup. A rationale for semantically enhanced library languages. LCSD05. October 2005.

This paper presents the rationale for a novel approach to providing expressive, teachable, maintainable, and cost-effective special-purpose languages: A Semantically Enhanced Library Language (a SEL language or a SELL) is a dialect created by supersetting a language using a library and then subsetting the result using a tool that “understands” the syntax and semantics of both the underlying language and the library.

How similar or different this idea really is compared to the facilities found in PLT Scheme and other previous apporaches to this issue?

Transactions are a hot topic in programming languages, especially with some exciting recent work on providing language support for STM ("Software Transaction Memory"). A new paper, A Concurrent Calculus with Atomic Transactions, by Acciai, Boreale & Dal Zilio, provides an extension of CCS, which they call ATCCS ("Atomic Transactions CCS"), with support for the primary operations of STM.

I was not aware of work on modelling transactions in process calculi, but the bibliography cites six works, five from the last three years, and a Montanari&co paper from 1990:

• 6. L. Bocchi, C. Laneve and G. Zavattaro. A Calculus for Long Running Transactions. In Proc. of FMOODS, LNCS 2884, 2003.

• 8. R. Bruni, H.C. Melgratti and U. Montanari. Nested Commits for Mobile Calculi: extending Join. In Proc. of IFIP TCS, 563-576, 2004.

• 9. R. Bruni, H.C. Melgratti and U. Montanari. Theoretical Foundations for Compensations in Flow Composition Languages. In Proc. of POPL, ACM Press, 209-220, 2005.

• 15. V. Danos and J. Krivine. Reversible Communicating System. In Proc. of CONCUR, LNCS 3170, 2004.

• 16. V. Danos and J. Krivine. Transactions in RCCS. In Proc. of CONCUR, LNCS 3653, 2005.

• 18. R. Gorrieri, S. Marchetti and U. Montanari. ACCS: Atomic
  Actions for CCS. Theoretical Computer Science,
  72(2-3):203-223, 1990.

I haven't read these papers, but from the summary in the concluding paper of the ABZ paper, there seem to be some interesting ideas floating about here. Will repay a closer look, I think...

It's been a while since I submitted a story...here is some food for thought!

What will programming look like in 20 years? Maybe it will be based on a "definitive language" like the speculations of the article Convergence in language design: a case of lightning striking four times in the same place (FLOPS 2006). Such a language will have a layered structure and its handling of concurrency is important. (Whether it is dynamically or statically typed is of absolutely no importance, BTW.)

How will we program with such a language? Maybe we will program with feedback loops, as explained in Self management and the future of software design (FACS 06). This seems to be one way to handle complexity, the inevitability of software and hardware faults, and managing global behavior of a system. I am coordinating a new project, SELFMAN, that is looking at this.

Comments?

Practical OCaml. Joshua Smith.

Apress has recently published a "mainstream" book (in English!) on OCaml. Here is an interview with the author, on a Ruby blog, of all places. I haven't seen the book yet, but will certainly buy it. If it's as good as Practical Common Lisp and generates as much buzz, this will be a very nice thing.

Two opposed views about the "no continuations in Ruby 2.0" announcement:

Patrick Logan: Ruby Sucks?

Don Box: Two Excellent Things for Ruby at Microsoft.

From the n-Category Cafe, some notes on Holodeck Games and cartesian closed categories.

This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both.

It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable.

Brendan Eich has just mentioned on the es4-discuss mailing list that we will be using ML as the definition language for the semantics of ECMAScript Edition 4. One of the immediate benefits of this approach will be that our definition will also serve as a reference implementation. LtUers will of course recognize this as the approach of "definitional interpreters" (discussed on LtU here and countless other times).

Our initial intention was to write a custom specification language that would be tailored to our purposes, with just the right core control features and datatypes to serve as an appropriately abstract model of ECMAScript. But before long, we realized that we were pretty much describing ML. Rather than specifying, implementing, and documenting another programming language that was 80% ML, why reinvent the wheel?

The benefits of this approach are many: a definition in a formal language that itself has a clear and precise definition, the luxury of many robust and high-performance implementations (we'll be using OCaml extended with first-class continuations), and free "technology transfer" from all the existing ML literature and communities.

And finally, by releasing real software--written in a direct functional style--for reading, type-checking, and evaluating ECMAScript programs, we'll be providing a standard set of tools for static analysis and other research on the ECMAScript language.

Ralph Griswold died two weeks ago. He created several programming languages, most notably Snobol (in the 60s) and Icon (in the 70s) — both outstandingly innovative, integral, and efficacious in their areas. Despite the abundance of scripting and other languages today, Snobol and Icon are still unsurpassed in many respects, both as elegance of design and as practicality.